The present invention relates to a static verification program, a static verification device, and a static verification method, and in particular to a static verification program, a static verification device, and a static verification method applied to verify operation of an integrated circuit.
Static verification is used as a technique for verifying operation of a circuit in a design of a large scale integrated circuit. As design verification workload increases in recent years, the static verification is regarded as indispensable. The static verification is a verification technique for mathematically verifying that described specification property (assertion) satisfies a design specification.
In the static verification, search is performed for all reachable state spaces that can be created by a state variable described in the specification property, and it is verified that the specification property is satisfied in each state space (Japanese Unexamined Patent Application Publication No. 2005-196681). Therefore, the static verification is better than logic simulation in terms of exhaustive verification.
In an actual EDA tool, as a static verification method, a symbolic model checking method is used (Masahiro Fujita, “[Special Lecture] SAT algorithm and its application on formal verification”, IEICE Technical Report, The Institute of Electronics, Information and Communication Engineers, November 2006, Vol. 106, No. 388, 391, 393, pp. 15-20). The symbolic model checking method is a method in which a state set and a state transition are symbolically represented by mathematical formulas and state search is performed by processing these formulas. In the symbolic model checking method, a certain state set is calculated as a product of a state set of the previous cycle and its state transition. Since the above operation is logic function processing, all operations can be processed as a BDD (Binary decision diagram) calculation or a SAT problem.
However, an amount of calculation in the static verification is greater than that in the logic simulation. Therefore, a huge calculation time is required depending on the scale of the circuit to be verified, so that it may prolong the verification time. Thus, a method is used in which an execution time limit of the static verification is set, and if the time limit is reached while verification result cannot be obtained, the static verification is forcibly terminated. To be exact, the verification is performed only on states that can be reached within the number of state transition cycles (search depth) that can be performed in a processing time (bounded model checking).